$\forall$$T$:Type, $P$:($T$$\rightarrow$Prop), $L$, ${\it L'}$:$T$ List. ($\forall$$x$$\in$$L$. $P$($x$)) $\Rightarrow$ $L$ $=$ ${\it L'}$ $\Rightarrow$ $L$ $=$ ${\it L'}$ $\in$ \{$x$:$T$$\mid$ $P$($x$) \} List